0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 17 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 674 ms)
↳10 BOUNDS(1, n^1)
natsFrom(N) → cons(N, n__natsFrom(s(N)))
fst(pair(XS, YS)) → XS
snd(pair(XS, YS)) → YS
splitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X, XS)) → u(splitAt(N, activate(XS)), N, X, activate(XS))
u(pair(YS, ZS), N, X, XS) → pair(cons(activate(X), YS), ZS)
head(cons(N, XS)) → N
tail(cons(N, XS)) → activate(XS)
sel(N, XS) → head(afterNth(N, XS))
take(N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → snd(splitAt(N, XS))
natsFrom(X) → n__natsFrom(X)
activate(n__natsFrom(X)) → natsFrom(X)
activate(X) → X
natsFrom(N) → cons(N, n__natsFrom(s(N))) [1]
fst(pair(XS, YS)) → XS [1]
snd(pair(XS, YS)) → YS [1]
splitAt(0, XS) → pair(nil, XS) [1]
splitAt(s(N), cons(X, XS)) → u(splitAt(N, activate(XS)), N, X, activate(XS)) [1]
u(pair(YS, ZS), N, X, XS) → pair(cons(activate(X), YS), ZS) [1]
head(cons(N, XS)) → N [1]
tail(cons(N, XS)) → activate(XS) [1]
sel(N, XS) → head(afterNth(N, XS)) [1]
take(N, XS) → fst(splitAt(N, XS)) [1]
afterNth(N, XS) → snd(splitAt(N, XS)) [1]
natsFrom(X) → n__natsFrom(X) [1]
activate(n__natsFrom(X)) → natsFrom(X) [1]
activate(X) → X [1]
natsFrom(N) → cons(N, n__natsFrom(s(N))) [1]
fst(pair(XS, YS)) → XS [1]
snd(pair(XS, YS)) → YS [1]
splitAt(0, XS) → pair(nil, XS) [1]
splitAt(s(N), cons(X, XS)) → u(splitAt(N, activate(XS)), N, X, activate(XS)) [1]
u(pair(YS, ZS), N, X, XS) → pair(cons(activate(X), YS), ZS) [1]
head(cons(N, XS)) → N [1]
tail(cons(N, XS)) → activate(XS) [1]
sel(N, XS) → head(afterNth(N, XS)) [1]
take(N, XS) → fst(splitAt(N, XS)) [1]
afterNth(N, XS) → snd(splitAt(N, XS)) [1]
natsFrom(X) → n__natsFrom(X) [1]
activate(n__natsFrom(X)) → natsFrom(X) [1]
activate(X) → X [1]
| natsFrom :: s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil cons :: s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil n__natsFrom :: s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil s :: s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil fst :: pair → s:n__natsFrom:cons:0:nil pair :: s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil → pair snd :: pair → s:n__natsFrom:cons:0:nil splitAt :: s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil → pair 0 :: s:n__natsFrom:cons:0:nil nil :: s:n__natsFrom:cons:0:nil u :: pair → s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil → pair activate :: s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil head :: s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil tail :: s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil sel :: s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil afterNth :: s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil take :: s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil → s:n__natsFrom:cons:0:nil |
fst(v0) → null_fst [0]
snd(v0) → null_snd [0]
splitAt(v0, v1) → null_splitAt [0]
u(v0, v1, v2, v3) → null_u [0]
head(v0) → null_head [0]
tail(v0) → null_tail [0]
null_fst, null_snd, null_splitAt, null_u, null_head, null_tail
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
nil => 1
null_fst => 0
null_snd => 0
null_splitAt => 0
null_u => 0
null_head => 0
null_tail => 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 1 }→ natsFrom(X) :|: z = 1 + X, X >= 0
afterNth(z, z') -{ 1 }→ snd(splitAt(N, XS)) :|: z' = XS, z = N, XS >= 0, N >= 0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
fst(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
head(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
natsFrom(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
natsFrom(z) -{ 1 }→ 1 + N + (1 + (1 + N)) :|: z = N, N >= 0
sel(z, z') -{ 1 }→ head(afterNth(N, XS)) :|: z' = XS, z = N, XS >= 0, N >= 0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
splitAt(z, z') -{ 1 }→ u(splitAt(N, activate(XS)), N, X, activate(XS)) :|: z = 1 + N, z' = 1 + X + XS, X >= 0, XS >= 0, N >= 0
splitAt(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
splitAt(z, z') -{ 1 }→ 1 + 1 + XS :|: z' = XS, z = 0, XS >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
tail(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
take(z, z') -{ 1 }→ fst(splitAt(N, XS)) :|: z' = XS, z = N, XS >= 0, N >= 0
u(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(X) + YS) + ZS :|: z = 1 + YS + ZS, z'' = X, YS >= 0, X >= 0, z' = N, z1 = XS, ZS >= 0, XS >= 0, N >= 0
| eq(start(V, V1, V2, V3),0,[natsFrom(V, Out)],[V >= 0]). eq(start(V, V1, V2, V3),0,[fst(V, Out)],[V >= 0]). eq(start(V, V1, V2, V3),0,[snd(V, Out)],[V >= 0]). eq(start(V, V1, V2, V3),0,[splitAt(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3),0,[u(V, V1, V2, V3, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0]). eq(start(V, V1, V2, V3),0,[head(V, Out)],[V >= 0]). eq(start(V, V1, V2, V3),0,[tail(V, Out)],[V >= 0]). eq(start(V, V1, V2, V3),0,[sel(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3),0,[take(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3),0,[afterNth(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3),0,[activate(V, Out)],[V >= 0]). eq(natsFrom(V, Out),1,[],[Out = 3 + 2*N1,V = N1,N1 >= 0]). eq(fst(V, Out),1,[],[Out = XS1,V = 1 + XS1 + YS1,YS1 >= 0,XS1 >= 0]). eq(snd(V, Out),1,[],[Out = YS2,V = 1 + XS2 + YS2,YS2 >= 0,XS2 >= 0]). eq(splitAt(V, V1, Out),1,[],[Out = 2 + XS3,V1 = XS3,V = 0,XS3 >= 0]). eq(splitAt(V, V1, Out),1,[activate(XS4, Ret01),splitAt(N2, Ret01, Ret0),activate(XS4, Ret3),u(Ret0, N2, X1, Ret3, Ret)],[Out = Ret,V = 1 + N2,V1 = 1 + X1 + XS4,X1 >= 0,XS4 >= 0,N2 >= 0]). eq(u(V, V1, V2, V3, Out),1,[activate(X2, Ret0101)],[Out = 2 + Ret0101 + YS3 + ZS1,V = 1 + YS3 + ZS1,V2 = X2,YS3 >= 0,X2 >= 0,V1 = N3,V3 = XS5,ZS1 >= 0,XS5 >= 0,N3 >= 0]). eq(head(V, Out),1,[],[Out = N4,V = 1 + N4 + XS6,XS6 >= 0,N4 >= 0]). eq(tail(V, Out),1,[activate(XS7, Ret1)],[Out = Ret1,V = 1 + N5 + XS7,XS7 >= 0,N5 >= 0]). eq(sel(V, V1, Out),1,[afterNth(N6, XS8, Ret02),head(Ret02, Ret2)],[Out = Ret2,V1 = XS8,V = N6,XS8 >= 0,N6 >= 0]). eq(take(V, V1, Out),1,[splitAt(N7, XS9, Ret03),fst(Ret03, Ret4)],[Out = Ret4,V1 = XS9,V = N7,XS9 >= 0,N7 >= 0]). eq(afterNth(V, V1, Out),1,[splitAt(N8, XS10, Ret04),snd(Ret04, Ret5)],[Out = Ret5,V1 = XS10,V = N8,XS10 >= 0,N8 >= 0]). eq(natsFrom(V, Out),1,[],[Out = 1 + X3,X3 >= 0,V = X3]). eq(activate(V, Out),1,[natsFrom(X4, Ret6)],[Out = Ret6,V = 1 + X4,X4 >= 0]). eq(activate(V, Out),1,[],[Out = X5,X5 >= 0,V = X5]). eq(fst(V, Out),0,[],[Out = 0,V4 >= 0,V = V4]). eq(snd(V, Out),0,[],[Out = 0,V5 >= 0,V = V5]). eq(splitAt(V, V1, Out),0,[],[Out = 0,V6 >= 0,V7 >= 0,V = V6,V1 = V7]). eq(u(V, V1, V2, V3, Out),0,[],[Out = 0,V3 = V8,V9 >= 0,V2 = V10,V11 >= 0,V = V9,V1 = V11,V10 >= 0,V8 >= 0]). eq(head(V, Out),0,[],[Out = 0,V12 >= 0,V = V12]). eq(tail(V, Out),0,[],[Out = 0,V13 >= 0,V = V13]). input_output_vars(natsFrom(V,Out),[V],[Out]). input_output_vars(fst(V,Out),[V],[Out]). input_output_vars(snd(V,Out),[V],[Out]). input_output_vars(splitAt(V,V1,Out),[V,V1],[Out]). input_output_vars(u(V,V1,V2,V3,Out),[V,V1,V2,V3],[Out]). input_output_vars(head(V,Out),[V],[Out]). input_output_vars(tail(V,Out),[V],[Out]). input_output_vars(sel(V,V1,Out),[V,V1],[Out]). input_output_vars(take(V,V1,Out),[V,V1],[Out]). input_output_vars(afterNth(V,V1,Out),[V,V1],[Out]). input_output_vars(activate(V,Out),[V],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [natsFrom/2]
1. non_recursive : [activate/2]
2. non_recursive : [snd/2]
3. non_recursive : [u/5]
4. recursive [non_tail] : [splitAt/3]
5. non_recursive : [afterNth/3]
6. non_recursive : [fst/2]
7. non_recursive : [head/2]
8. non_recursive : [sel/3]
9. non_recursive : [tail/2]
10. non_recursive : [take/3]
11. non_recursive : [start/4]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into natsFrom/2
1. SCC is partially evaluated into activate/2
2. SCC is partially evaluated into snd/2
3. SCC is partially evaluated into u/5
4. SCC is partially evaluated into splitAt/3
5. SCC is partially evaluated into afterNth/3
6. SCC is partially evaluated into fst/2
7. SCC is partially evaluated into head/2
8. SCC is partially evaluated into sel/3
9. SCC is partially evaluated into tail/2
10. SCC is partially evaluated into take/3
11. SCC is partially evaluated into start/4
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations natsFrom/2
* CE 13 is refined into CE [33]
* CE 14 is refined into CE [34]
### Cost equations --> "Loop" of natsFrom/2
* CEs [33] --> Loop 22
* CEs [34] --> Loop 23
### Ranking functions of CR natsFrom(V,Out)
#### Partial ranking functions of CR natsFrom(V,Out)
### Specialization of cost equations activate/2
* CE 31 is refined into CE [35,36]
* CE 32 is refined into CE [37]
### Cost equations --> "Loop" of activate/2
* CEs [36] --> Loop 24
* CEs [35,37] --> Loop 25
### Ranking functions of CR activate(V,Out)
#### Partial ranking functions of CR activate(V,Out)
### Specialization of cost equations snd/2
* CE 17 is refined into CE [38]
* CE 18 is refined into CE [39]
### Cost equations --> "Loop" of snd/2
* CEs [38] --> Loop 26
* CEs [39] --> Loop 27
### Ranking functions of CR snd(V,Out)
#### Partial ranking functions of CR snd(V,Out)
### Specialization of cost equations u/5
* CE 22 is refined into CE [40,41]
* CE 23 is refined into CE [42]
### Cost equations --> "Loop" of u/5
* CEs [41] --> Loop 28
* CEs [40] --> Loop 29
* CEs [42] --> Loop 30
### Ranking functions of CR u(V,V1,V2,V3,Out)
#### Partial ranking functions of CR u(V,V1,V2,V3,Out)
### Specialization of cost equations splitAt/3
* CE 21 is refined into CE [43]
* CE 19 is refined into CE [44]
* CE 20 is refined into CE [45,46,47,48,49,50,51,52,53,54,55,56]
### Cost equations --> "Loop" of splitAt/3
* CEs [53,56] --> Loop 31
* CEs [46,49] --> Loop 32
* CEs [47,50] --> Loop 33
* CEs [52,55] --> Loop 34
* CEs [51,54] --> Loop 35
* CEs [45,48] --> Loop 36
* CEs [43] --> Loop 37
* CEs [44] --> Loop 38
### Ranking functions of CR splitAt(V,V1,Out)
* RF of phase [31,32,33,34]: [V]
* RF of phase [35,36]: [V]
#### Partial ranking functions of CR splitAt(V,V1,Out)
* Partial RF of phase [31,32,33,34]:
- RF of loop [31:1,32:1,33:1,34:1]:
V
- RF of loop [32:1]:
V1 depends on loops [31:1,34:1]
- RF of loop [33:1]:
V1/2-1/2 depends on loops [31:1,34:1]
* Partial RF of phase [35,36]:
- RF of loop [35:1,36:1]:
V
- RF of loop [36:1]:
V1 depends on loops [35:1]
### Specialization of cost equations afterNth/3
* CE 30 is refined into CE [57,58,59,60,61]
### Cost equations --> "Loop" of afterNth/3
* CEs [61] --> Loop 39
* CEs [59,60] --> Loop 40
* CEs [57,58] --> Loop 41
### Ranking functions of CR afterNth(V,V1,Out)
#### Partial ranking functions of CR afterNth(V,V1,Out)
### Specialization of cost equations fst/2
* CE 15 is refined into CE [62]
* CE 16 is refined into CE [63]
### Cost equations --> "Loop" of fst/2
* CEs [62] --> Loop 42
* CEs [63] --> Loop 43
### Ranking functions of CR fst(V,Out)
#### Partial ranking functions of CR fst(V,Out)
### Specialization of cost equations head/2
* CE 24 is refined into CE [64]
* CE 25 is refined into CE [65]
### Cost equations --> "Loop" of head/2
* CEs [64] --> Loop 44
* CEs [65] --> Loop 45
### Ranking functions of CR head(V,Out)
#### Partial ranking functions of CR head(V,Out)
### Specialization of cost equations sel/3
* CE 28 is refined into CE [66,67,68,69,70]
### Cost equations --> "Loop" of sel/3
* CEs [70] --> Loop 46
* CEs [68,69] --> Loop 47
* CEs [66,67] --> Loop 48
### Ranking functions of CR sel(V,V1,Out)
#### Partial ranking functions of CR sel(V,V1,Out)
### Specialization of cost equations tail/2
* CE 26 is refined into CE [71,72]
* CE 27 is refined into CE [73]
### Cost equations --> "Loop" of tail/2
* CEs [72] --> Loop 49
* CEs [71] --> Loop 50
* CEs [73] --> Loop 51
### Ranking functions of CR tail(V,Out)
#### Partial ranking functions of CR tail(V,Out)
### Specialization of cost equations take/3
* CE 29 is refined into CE [74,75,76,77,78]
### Cost equations --> "Loop" of take/3
* CEs [78] --> Loop 52
* CEs [76,77] --> Loop 53
* CEs [74,75] --> Loop 54
### Ranking functions of CR take(V,V1,Out)
#### Partial ranking functions of CR take(V,V1,Out)
### Specialization of cost equations start/4
* CE 2 is refined into CE [79,80]
* CE 3 is refined into CE [81,82]
* CE 4 is refined into CE [83,84]
* CE 5 is refined into CE [85,86,87]
* CE 6 is refined into CE [88,89,90]
* CE 7 is refined into CE [91,92]
* CE 8 is refined into CE [93,94,95]
* CE 9 is refined into CE [96,97,98]
* CE 10 is refined into CE [99,100,101]
* CE 11 is refined into CE [102,103,104]
* CE 12 is refined into CE [105,106]
### Cost equations --> "Loop" of start/4
* CEs [79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106] --> Loop 55
### Ranking functions of CR start(V,V1,V2,V3)
#### Partial ranking functions of CR start(V,V1,V2,V3)
Computing Bounds
=====================================
#### Cost of chains of natsFrom(V,Out):
* Chain [23]: 1
with precondition: [V+1=Out,V>=0]
* Chain [22]: 1
with precondition: [2*V+3=Out,V>=0]
#### Cost of chains of activate(V,Out):
* Chain [25]: 2
with precondition: [V=Out,V>=0]
* Chain [24]: 2
with precondition: [2*V+1=Out,V>=1]
#### Cost of chains of snd(V,Out):
* Chain [27]: 0
with precondition: [Out=0,V>=0]
* Chain [26]: 1
with precondition: [Out>=0,V>=Out+1]
#### Cost of chains of u(V,V1,V2,V3,Out):
* Chain [30]: 0
with precondition: [Out=0,V>=0,V1>=0,V2>=0,V3>=0]
* Chain [29]: 3
with precondition: [V+V2+1=Out,V>=1,V1>=0,V2>=0,V3>=0]
* Chain [28]: 3
with precondition: [V+2*V2+2=Out,V>=1,V1>=0,V2>=1,V3>=0]
#### Cost of chains of splitAt(V,V1,Out):
* Chain [[35,36],[31,32,33,34],38]: 42*it(31)+1
Such that:aux(32) =< V
it(31) =< aux(32)
with precondition: [Out=0,V>=2,V1>=2]
* Chain [[35,36],38]: 10*it(35)+1
Such that:aux(33) =< V
it(35) =< aux(33)
with precondition: [Out=0,V>=1,V1>=1]
* Chain [[35,36],37]: 10*it(35)+0
Such that:aux(34) =< V
it(35) =< aux(34)
with precondition: [Out=0,V>=1,V1>=1]
* Chain [[31,32,33,34],38]: 32*it(31)+1
Such that:aux(23) =< V
it(31) =< aux(23)
with precondition: [V>=1,V1>=1,Out>=V1+2]
* Chain [38]: 1
with precondition: [V=0,V1+2=Out,V1>=0]
* Chain [37]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of afterNth(V,V1,Out):
* Chain [41]: 3
with precondition: [V=0,V1>=0,Out>=0,V1+1>=Out]
* Chain [40]: 94*s(8)+2
Such that:aux(36) =< V
s(8) =< aux(36)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [39]: 32*s(12)+3
Such that:s(11) =< V
s(12) =< s(11)
with precondition: [V>=1,V1>=1,Out>=0]
#### Cost of chains of fst(V,Out):
* Chain [43]: 0
with precondition: [Out=0,V>=0]
* Chain [42]: 1
with precondition: [Out>=0,V>=Out+1]
#### Cost of chains of head(V,Out):
* Chain [45]: 0
with precondition: [Out=0,V>=0]
* Chain [44]: 1
with precondition: [Out>=0,V>=Out+1]
#### Cost of chains of sel(V,V1,Out):
* Chain [48]: 5
with precondition: [V=0,Out>=0,V1>=Out]
* Chain [47]: 126*s(14)+4
Such that:aux(37) =< V
s(14) =< aux(37)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [46]: 32*s(18)+5
Such that:s(17) =< V
s(18) =< s(17)
with precondition: [V>=1,V1>=1,Out>=0]
#### Cost of chains of tail(V,Out):
* Chain [51]: 0
with precondition: [Out=0,V>=0]
* Chain [50]: 3
with precondition: [Out>=0,V>=Out+1]
* Chain [49]: 3
with precondition: [Out>=3,2*V>=Out+1]
#### Cost of chains of take(V,V1,Out):
* Chain [54]: 3
with precondition: [V=0,V1>=0,Out>=0,V1+1>=Out]
* Chain [53]: 94*s(20)+2
Such that:aux(38) =< V
s(20) =< aux(38)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [52]: 32*s(24)+3
Such that:s(23) =< V
s(24) =< s(23)
with precondition: [V>=1,V1>=1,Out>=0]
#### Cost of chains of start(V,V1,V2,V3):
* Chain [55]: 504*s(26)+5
Such that:aux(39) =< V
s(26) =< aux(39)
with precondition: [V>=0]
Closed-form bounds of start(V,V1,V2,V3):
-------------------------------------
* Chain [55] with precondition: [V>=0]
- Upper bound: 504*V+5
- Complexity: n
### Maximum cost of start(V,V1,V2,V3): 504*V+5
Asymptotic class: n
* Total analysis performed in 526 ms.